package trabajoISW2.domain.contracts;

import java.util.List;

import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Query;
import trabajoISW2.domain.implementations.Detail;
import trabajoISW2.domain.models.ICartModel;

@Inv({"getAmount() == calculateAmount(getDetails())"})
public interface ICart extends ICartModel{
	
	
	@Pre("details !=null #IllegalArgumentException")
	@Pos("getDetails().compare(details) == 0")
	public void setDetails (List<Detail> details);
	
	@Query
	public List<Detail> getDetails();
	
	@Pre({"detail !=null #IllegalArgumentException","getDetails().size()<Integer.MAX_VALUE #IllegalArgumentException"})
	@Pos({"!getDetails().contains(detail) ==> getDetails().size() == getDetails()@pre.size() +1",
		"getDetails().contains(detail) ==> getDetail(detail.getItemID).getQuantity() == getDetail(detail.getItemID).getQuantity()@pre + detail.getQuantity"	})
	public boolean addDetail(Detail detail);
	
	@Pre({"itemId >= 0 #IllegalArgumentException", "itemID <= Integer.MAX_VALUE #IllegalArgumentException"})
	@Pos("getDetails().size() == getDetails()@pre.size() -1")
	public boolean removeDetail(int itemId);
	
	
	@Pre({"itemId >= 0  && itemId <= Integer.MAX_VALUE #IllegalArgumentException", 
		"quantity >= 0 && quantity <= Integer.Max-value #IllegalArgumentException"	})
	@Pos("getItem(itemId).getQuantity() == quantity")
	public boolean modifyDetail(int DetailId,int quantity);
	
	@Query
	public Detail getDetail(int itemId);	
	
	@Query
	public double getAmount();
}
